Skip to content

Simplifications to partial_eval_preserves_typeof#896

Merged
john-h-kastner-aws merged 2 commits intomainfrom
pe-preserves-type-of
Mar 5, 2026
Merged

Simplifications to partial_eval_preserves_typeof#896
john-h-kastner-aws merged 2 commits intomainfrom
pe-preserves-type-of

Conversation

@john-h-kastner-aws
Copy link
Copy Markdown
Contributor

@john-h-kastner-aws john-h-kastner-aws commented Mar 4, 2026

Issue #, if available:

Description of changes:

@john-h-kastner-aws
minor simplifications to partial_eval_preserves_typeof
e4a29f4 
Signed-off-by: John Kastner <jkastner@amazon.com>
Copilot AI reviewed Mar 4, 2026
View reviewed changes
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR refactors the partial_eval_preserves_typeof theorem to a simpler statement (PEPreservesTypeOf res) that depends only on Residual.WellTyped and the chosen (preq, pes), and then updates downstream well-typedness lemmas to use the new interface.

Changes:

  • Redefines PEPreservesTypeOf to quantify over {env} and (preq, pes), and restates partial_eval_preserves_typeof as ∀ res, PEPreservesTypeOf res.
  • Updates partial_eval_preserves_typeof_* helper proofs to match the new PEPreservesTypeOf signature.
  • Adjusts many call sites in WellTypedCases.lean to the new partial_eval_preserves_typeof API.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 20 comments.

File Description
cedar-lean/Cedar/Thm/TPE/WellTypedCases.lean Updates numerous proof steps to use the new partial_eval_preserves_typeof signature.
cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean Refactors the main preservation theorem and its helpers to a simplified PEPreservesTypeOf formulation.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@john-h-kastner-aws
tweak
a8f5687 
Signed-off-by: John Kastner <jkastner@amazon.com>
cdisselkoen
cdisselkoen approved these changes Mar 5, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@cdisselkoen cdisselkoen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great simplification. I assume you checked whether we can remove any hypotheses from the proofs up the stack, similar to how we're removing unneeded hypotheses from this definition?

cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean
RequestAndEntitiesRefine req es preq pes →
Residual.WellTyped env res →
(TPE.evaluate res preq pes).typeOf = res.typeOf
abbrev PEPreservesTypeOf (res : Residual) : Prop :=
Copy link
Copy Markdown
Contributor

@cdisselkoen cdisselkoen Mar 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not related to this PR, but -- curious why this is abbrev instead of def?

Copy link
Copy Markdown
Contributor Author

@john-h-kastner-aws john-h-kastner-aws Mar 5, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It compiles with def, so idk. Quick search says Lean is more willing to automatically unfold abbrevs.

@john-h-kastner-aws
Copy link
Copy Markdown
Contributor Author

john-h-kastner-aws commented Mar 5, 2026

whether we can remove any hypotheses from the proofs up the stack

I feel like I shouldn't need RequestAndEntitiesRefine to prove partial_eval_preserves_well_typed. Why should the concrete request matter for a property purely about partial eval? The current proof does use it though, so it's not a trivial change. I think I'd need define a variant of InstanceOfWellFormedEnvironment for partial requests directly since InstanceOfWellFormedEnvironment env req ∧ RequestAndEntitiesRefine preq req is currently used to say that the partial request is well formed.

@john-h-kastner-aws john-h-kastner-aws merged commit 4134dc2 into main Mar 5, 2026
12 of 13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

@cdisselkoen cdisselkoen cdisselkoen approved these changes

@victornicolet victornicolet victornicolet approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@john-h-kastner-aws @cdisselkoen @victornicolet